T:Type, L:T List, P:(TProp).
(x:T. Dec(P(x)))
 (L1, L2:T List.
 (interleaving(T;L1;L2;L)
 (& (x:T. (x  L1)  (x  L) & P(x))
 (& (x:T. (x  L2)  (x  L) & P(x))) 

latex

Definitions	t  T, x:A. B(x), P  Q, P  Q, P & Q, P  Q, False, x(s), interleaving(T;L1;L2;L), A, Prop, (x  l), x. t(x), x:A. B(x), Dec(P), P  Q, {T}, SQType(T), True
Lemmas	interleaving symmetry, cons interleaving, cons member, decidable wf, all functionality wrt iff, iff functionality wrt iff, and functionality wrt iff, nil member, l member wf, iff wf, interleaving wf, not wf, false wf, nil interleaving